a:Id, T:Top, ds:x:Id fp Type, P:Top, init:x:Id fp Top, a1:Id, T1:Top, d1:x:Id fp Type, P1:Top.
ds || d1
 a = a1
 (with ds: ds init: initaction a:T precondition a(v) is P
 (||+ (with ds: d1
 (||+ (action a1:T1
 (||+ (precondition a1(v) is
 (||+ (P1 s v)) 

latex

Definitions

A ||+ B, M1 || M2, M1 ||decl M2, Valtype(da;k), State(ds), rcv(l,tg), A & B, with ds: ds init: initaction a:T precondition a(v) is P, (with ds: ds action a:T precondition a(v) is P s v), x : v, , mk-ma, ma-frame-compatible(A;B), ma-frame-compat(A;B), M.rframe(A.pre p for a), M.rframe(A.effect f of k on y), M.rframe(A.sends tfL of k on l), xdom(f). v=f(x)   P(x;v), Void, M.aframe(k affects x), M.frame(k affects x), IdLnk, xL. P(x), M.dout(l,tg), (s1  s2 mod x), M.da(a), M.state, M.sframe(k sends <l,tg>), if b t else f fi, Case b of inl(x)  s(x) ; inr(y)  t(y), a:A fp B(a), x:A. B(x), f || g, x  dom(f), f(x), p  q, a = b, EqDecider(T), eqof(d), false, P  Q, left+right, x. t(x), {T}, P  Q, P  Q, P & Q, b, deq-member(eq;x;L), (x  l), IdDeq, type List, 1of(t), f(a), 2of(t), x:AB(x), , {x:A| B(x) }, , AB, s = t, Prop, Type, f(x)?z, Top, f  g, KindDeq, car.cdr, nil, locl(a), x.A(x), Knd, <a,b>, Id, x:A. B(x), x:AB(x), t  T, A, P  Q, False

Lemmas

locl one one, Id wf, id-deq wf, l member wf, deq-member wf, assert wf, assert-deq-member, and functionality wrt iff, implies functionality wrt iff, all functionality wrt iff, deq property, bfalse wf, eqof wf, assert of bor, Knd wf, locl wf, Kind-deq wf, false wf, eq id wf, bor wf, assert-eq-id, or functionality wrt iff, iff transitivity, IdLnk wf, top wf, fpf wf, fpf-compatible wf, not wf